This disclosure teaches a technique for dynamically removing inactive clauses in a Boolean satisfiability checking (SAT) problem. While, specific example circuit types might be discussed to better understand the disclosed technique, the technique itself is applicable to any circuit analysis problem that uses SAT. The precise scope of the disclosed technique should be self-evident from the claims.
1. References
The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [2] for the second numbered paper by A. Biere et al.):
[1] M. Abramovici, M. A. Bruer, and A. D. Friedman. Digital Systems Testing and testable Design. Electrical Engineering, Communications and Signal Processing. Computer Science Press, New York, N.Y., 1990.
[2] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, 1999.
[3] R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proceedings of the Internation Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 428-432, June 1996.
[4] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.
[5]. Burch and V. Singhal. Tight integration of combinational verification methods. In Proceedings of the International Conference on Computer-Aided Design, pages 570-576, 1998.
[6]. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design, 13(4):401-424, April 1994.
[7] S. T. Chakradhar, V. D. Agrawal, and S. G. Rothweiler. A transitive closure algorithm for test generation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 12(1): 1015-1028, July 1993.
[8] Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proceedings of the International Conference on Computer-Aided Verification (CAV 90), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1991.
[9] A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proceedings of the VLSI Design Conference, January 1998.
[10] A. Gupta, Z. Yang, A. Gupta, and P. Ashar. Sat-based image computation with application in reachability analysis. In Formal Methods in Computer-Aided Design, 2000.
[11] W. Kunz and D. Pradhan. Recursive learning: A new implication technique for efficient solutions to cad problemsxe2x80x94test, verification and optimization. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(9):1143-1158, September 1994.
[12] T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1l(l):4-15, January 1992.
[13] J. P. Marques-Silva and A. L. Oliveira. Improving satisfiability algorithms with dominance and partitioning. In IEEE/ACM International Workshop on Logic Synthesis, May 1997.
[14] J. P. Marques-Silva and K. A. Sakallah. Grasp: A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, pages 220-227, November 1996.
[15] J. P. Marquez-Silva. Grasp package. http://algos.inesc.pt/xcx9cjpms/software.html.
[16] I.-H. Moon, G. Hachtel, and F. Somenzi. Border-clock triangular form and conjunction schedule in image computation. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, 2000.
[17] I.-H. Moon, J. Kukula, K. Ravi, and F Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23-28, June 2000.
[18] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering a (super?) efficient SAT solver. In Proceedings of the Design Automation Conference, 2001.
[19] M. Sheeran and G. Stalmark. A tutorial on Stalmark""s method of propositional proof. Formal Methods in System Design, 16(1), 2000.
[20] O. Shtrichman. Tuning SAT checkers for bounded model checking. In proceedings of the International Conference on Computer-Aided Verification, 2000.
[21] F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package. http://visi.colorado.edu/xcx9cfabio/CUDD/.
[22] H. Zhang. SATO: an efficient propositional prover. In International Conference on Automated Deduction, number 1249 in LNAI, pages 272-275, 1997.
2. Related Work
Checking Boolean Satisfiability (SAT) is required for a number of applications in VLSI CAD including combinational verification, Automatic Test Pattern Generation (ATPG), timing analysis, synthesis and, recently, reachability analysis and model checking. Acceleration of SAT can have significant impact in terms of improving the quality of these applications. SAT has received considerable attention in the recent past, focusing both on basic improvements in the SAT algorithms [7, 11, 14, 19], and on various applications like Automatic Test Pattern Generation (ATPG) [12], equivalence checking [5, 9], bounded model checking (BMC) [2]. Recently, combining SAT techniques with BDDs has been shown to be effective for image computation with application in state reachability analysis of sequential circuits [10].
Typical SAT solvers are based on a Davis-Putnam style branch-and-bound algorithm, and include considerable sophistication in heuristics for decision making, implication gathering, and backtracking [15, 18, 22]. However, missing from these efforts is exploitation of the fact that most SAT problems arising in VLSI CAD are derived from logic gate netlists. Logic gate netlists have some special properties related to how gates are connected together to realize circuit functionality. These include properties like the input-to-output flow of information, limitation on the fanout and fanin of each gate, and the connectivity and signal value dependence dynamically changing the controllability and observability of a gate. Such properties have not been exploited in conventional SAT packages.
On the other hand, circuit structure has been effectively utilized in many SAT applications, e.g., ATPG [1], BMC [20]. However, this utilization has been mostly application-specific. For example, justification/propagation frontiers in ATPG, and unrolled transition relations in BMC, are used for more effective decision heuristics in the associated SAT procedures.
While the technique disclosed herein provide a clear benefit to SAT algorithms, it is also important to put the disclosed ideas in the context of the large body of work in conventional combinational ATPG [1]. Unlike traditional SAT, conventional ATPG algorithms operate on data structures at the level of the circuit structure itself. As a result, all circuit information, including gate connectivity, is directly available to these algorithms. In-deed, dynamic detection of inactive circuit regions is performed by the justification-propagation operations, which are at the core of ATPG algorithms. However, there is no explicit removal of these inactive regions. In particular, the overhead of propagating values through inactive regions is not avoided.
In terms of detecting redundant clauses in a SAT formula, a recent effort [13] proposed the use of clause dominance in the inner loop of the SAT algorithm. Unfortunately, the effort required for detection of dominating clauses is high, and it typically negates the gains arising out of clause removal.
However, circuit structures can be advantageously exploited in order to improve the performance of generic SAT applications arising in VLSI CAD. In particular, the notion of unobservability of gates at circuit outputs can be advantageously used to reduce the size of the SAT sub-problems. It is well known that, like all search algorithms, the effectiveness of a SAT algorithm is based on the amount of pruning of the search space it enables. The amount of pruning, in turn, is directly affected by the decision making heuristics and implication methods. Typically, their effectiveness is inversely proportional to the size of the SAT problem. Thus, the size of a SAT problem affects not only the size of the search space, but also the effectiveness of pruning methods. Therefore, it is generally advantageous to reduce the size of the SAT problem.
The disclosed techniques are aimed at realizing the advantages mentioned above.
3. Image Computation Using SAT
This sub-section describes image computation using SAT. The background information provided in this section will assist in understanding the Experimental Results described in Section IV.D. Historically, symbolic state space traversal [6, 8] has relied on efficient algorithms based on BDDs [4] for carrying out an image computation, shown below:
Image (P,T)(y)=∃x,iT(x, i, y){circumflex over ( )}P(X)xe2x80x83xe2x80x83(1)
Here, x/y denote present/next state variables, i denotes primary input variables, T denotes the transition relation, and P denotes the input state set. BDDs are used to represent the characteristic function of the transition relation, as well as the input/image sets. As an example application, the set of reachable states can be computed by starting from a set P which denotes the set of initial states of a system, and using image computation iteratively, until a fixpoint is reached. The BDD-based approaches work well when it is possible to represent the sets of states and the transition relation (as a whole, or in a usefully partitioned form) using BDDs. Unfortunately, BDD size is very sensitive to the number of variables, variable ordering, and the nature of the logic expressions being represented.
Recently, an integration of SAT and BDDs has been proposed for image computation [10], which represents the transition relation as a CNF formula, and organizes the search for solutions as a top-level SAT search. BDD-based sub-problems are invoked on-the-fly, in order to obtain multiple solutions simultaneously. Section IV.D describes experimental results for reachability analysis according to the disclosed technique based on this image computation engine.
To achieve the advantages mentioned above there is provided a method of Boolean satisfiability checking (SAT) for a circuit. The method comprises identifying inactive clauses in the conjunctive normal form (CNF) of the circuit and removing the inactive clauses from the CNF.
According to another aspect, there is provided a method of reducing a size of a Boolean satisfiability checking (SAT) problem. The method comprises tagging variables and clauses of a conjunctive normal form (CNF) of a circuit once during a generation of the CNF description, the tagging being done based on a connectivity information of the circuit. The tagged information is used to perform backward traversals on the CNF description to remove inactive clauses.
In a further refinement, the inactive clauses are detected by marking all clauses and variables in a worst case.
In a still further refinement the inactive clauses are based on dynamic values of the variables, whereby whether a clause is inactive can change dynamically with the assigned value of a variable.
In a still further refinement, the detection is performed in an inner loop of the SAT search.
In a further refinement the tagging for a selected variable is performed by associating a fan-in list of clauses corresponding to a gate for which the selected variable represents an output, and recursively handling inputs for the gate in a similar manner.
In a still further refinement, the detection of inactive clauses are performed by a sub-process comprising adding all variables of interest to an active variable set. A variable is selected from the active variable set. A recursive backward traversal is performed for the selected variable. Clauses in a fan-in list associated with the selected variable are then looped over. Clauses that are looped over are marked as active. If an active clause is unsatisfied, all variables appearing in that clause are added to the active variable set. If an active clause is satisfied, only those variables in the clause that have assigned values are added to the active variable set. The steps are repeated for all unselected variables in the active variable set. All the unmarked clauses at the end are designated as inactive.
According to yet another aspect there is provided a method of solving an image computation problem using Boolean satisfiability checking (SAT) and binary decision diagrams (BDD), wherein at least one of the SAT checking and the associated BDD sub-problems is reduced by a process comprising tagging variables and clauses of a conjunctive normal form (CNF) of a circuit once during a generation of the CNF description , the tagging being done based on a connectivity information of the circuit and using the tagged information to perform backward traversals on the CNF description to remove inactive clauses.
In a further refinement, the inactive clauses are detected by marking all clauses and variables in a worst case.
In a still further refinement the inactive clauses are based on dynamic values of the variables, whereby whether a clause is inactive can change dynamically with the assigned value of a variable.
In a still further refinement, the detection is performed in an inner loop of the SAT search.
In a further refinement the tagging for a selected variable is performed by associating a fan-in list of clauses corresponding to a gate for which the selected variable represents an output, and recursively handling inputs for the gate in a similar manner.
In a still further refinement, the detection of inactive clauses are performed by a sub-process comprising adding all variables of interest to an active variable set. A variable is selected from the active variable set. A recursive backward traversal is performed for the selected variable. Clauses in a fan-in list associated with the selected variable are then looped over. Clauses that are looped over are marked as active. If an active clause is unsatisfied, all variables appearing in that clause are added to the active variable set. If an active clause is satisfied, only those variables in the clause that have assigned values are added to the active variable set. The steps are repeated for all unselected variables in the active variable set. All the unmarked clauses at the end are designated as inactive.